WORST_CASE(?,O(n^2))
* Step 1: DependencyPairs WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
add#2(Zero(),x8) -> x8
eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
eval#1(Nat(x1)) -> x1
eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
main(x12) -> eval#1(x12)
sub#2(x8,Zero()) -> x8
sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
sub#2(Zero(),Succ(x16)) -> Zero()
- Signature:
{add#2/2,eval#1/1,main/1,sub#2/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {add#2,eval#1,main,sub#2} and constructors {Add,Nat,Sub
,Succ,Zero}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
add#2#(Zero(),x8) -> c_2()
eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
eval#1#(Nat(x1)) -> c_4()
eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
main#(x12) -> c_6(eval#1#(x12))
sub#2#(x8,Zero()) -> c_7()
sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
sub#2#(Zero(),Succ(x16)) -> c_9()
Weak DPs
and mark the set of starting terms.
* Step 2: PredecessorEstimation WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
add#2#(Zero(),x8) -> c_2()
eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
eval#1#(Nat(x1)) -> c_4()
eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
main#(x12) -> c_6(eval#1#(x12))
sub#2#(x8,Zero()) -> c_7()
sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
sub#2#(Zero(),Succ(x16)) -> c_9()
- Weak TRS:
add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
add#2(Zero(),x8) -> x8
eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
eval#1(Nat(x1)) -> x1
eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
main(x12) -> eval#1(x12)
sub#2(x8,Zero()) -> x8
sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
sub#2(Zero(),Succ(x16)) -> Zero()
- Signature:
{add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
,c_1/1,c_2/0,c_3/3,c_4/0,c_5/3,c_6/1,c_7/0,c_8/1,c_9/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {add#2#,eval#1#,main#,sub#2#} and constructors {Add,Nat
,Sub,Succ,Zero}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{2,4,7,9}
by application of
Pre({2,4,7,9}) = {1,3,5,6,8}.
Here rules are labelled as follows:
1: add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
2: add#2#(Zero(),x8) -> c_2()
3: eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
4: eval#1#(Nat(x1)) -> c_4()
5: eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
6: main#(x12) -> c_6(eval#1#(x12))
7: sub#2#(x8,Zero()) -> c_7()
8: sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
9: sub#2#(Zero(),Succ(x16)) -> c_9()
* Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
main#(x12) -> c_6(eval#1#(x12))
sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
- Weak DPs:
add#2#(Zero(),x8) -> c_2()
eval#1#(Nat(x1)) -> c_4()
sub#2#(x8,Zero()) -> c_7()
sub#2#(Zero(),Succ(x16)) -> c_9()
- Weak TRS:
add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
add#2(Zero(),x8) -> x8
eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
eval#1(Nat(x1)) -> x1
eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
main(x12) -> eval#1(x12)
sub#2(x8,Zero()) -> x8
sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
sub#2(Zero(),Succ(x16)) -> Zero()
- Signature:
{add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
,c_1/1,c_2/0,c_3/3,c_4/0,c_5/3,c_6/1,c_7/0,c_8/1,c_9/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {add#2#,eval#1#,main#,sub#2#} and constructors {Add,Nat
,Sub,Succ,Zero}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
-->_1 add#2#(Zero(),x8) -> c_2():6
-->_1 add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2)):1
2:S:eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
-->_3 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):3
-->_2 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):3
-->_3 eval#1#(Nat(x1)) -> c_4():7
-->_2 eval#1#(Nat(x1)) -> c_4():7
-->_1 add#2#(Zero(),x8) -> c_2():6
-->_3 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
-->_2 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
-->_1 add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2)):1
3:S:eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
-->_1 sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2)):5
-->_1 sub#2#(Zero(),Succ(x16)) -> c_9():9
-->_1 sub#2#(x8,Zero()) -> c_7():8
-->_3 eval#1#(Nat(x1)) -> c_4():7
-->_2 eval#1#(Nat(x1)) -> c_4():7
-->_3 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):3
-->_2 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):3
-->_3 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
-->_2 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
4:S:main#(x12) -> c_6(eval#1#(x12))
-->_1 eval#1#(Nat(x1)) -> c_4():7
-->_1 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):3
-->_1 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
5:S:sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
-->_1 sub#2#(Zero(),Succ(x16)) -> c_9():9
-->_1 sub#2#(x8,Zero()) -> c_7():8
-->_1 sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2)):5
6:W:add#2#(Zero(),x8) -> c_2()
7:W:eval#1#(Nat(x1)) -> c_4()
8:W:sub#2#(x8,Zero()) -> c_7()
9:W:sub#2#(Zero(),Succ(x16)) -> c_9()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
7: eval#1#(Nat(x1)) -> c_4()
8: sub#2#(x8,Zero()) -> c_7()
9: sub#2#(Zero(),Succ(x16)) -> c_9()
6: add#2#(Zero(),x8) -> c_2()
* Step 4: RemoveHeads WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
main#(x12) -> c_6(eval#1#(x12))
sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
- Weak TRS:
add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
add#2(Zero(),x8) -> x8
eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
eval#1(Nat(x1)) -> x1
eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
main(x12) -> eval#1(x12)
sub#2(x8,Zero()) -> x8
sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
sub#2(Zero(),Succ(x16)) -> Zero()
- Signature:
{add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
,c_1/1,c_2/0,c_3/3,c_4/0,c_5/3,c_6/1,c_7/0,c_8/1,c_9/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {add#2#,eval#1#,main#,sub#2#} and constructors {Add,Nat
,Sub,Succ,Zero}
+ Applied Processor:
RemoveHeads
+ Details:
Consider the dependency graph
1:S:add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
-->_1 add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2)):1
2:S:eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
-->_3 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):3
-->_2 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):3
-->_3 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
-->_2 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
-->_1 add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2)):1
3:S:eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
-->_1 sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2)):5
-->_3 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):3
-->_2 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):3
-->_3 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
-->_2 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
4:S:main#(x12) -> c_6(eval#1#(x12))
-->_1 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):3
-->_1 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
5:S:sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
-->_1 sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2)):5
Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts).
[(4,main#(x12) -> c_6(eval#1#(x12)))]
* Step 5: UsableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
- Weak TRS:
add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
add#2(Zero(),x8) -> x8
eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
eval#1(Nat(x1)) -> x1
eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
main(x12) -> eval#1(x12)
sub#2(x8,Zero()) -> x8
sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
sub#2(Zero(),Succ(x16)) -> Zero()
- Signature:
{add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
,c_1/1,c_2/0,c_3/3,c_4/0,c_5/3,c_6/1,c_7/0,c_8/1,c_9/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {add#2#,eval#1#,main#,sub#2#} and constructors {Add,Nat
,Sub,Succ,Zero}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
add#2(Zero(),x8) -> x8
eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
eval#1(Nat(x1)) -> x1
eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
sub#2(x8,Zero()) -> x8
sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
sub#2(Zero(),Succ(x16)) -> Zero()
add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
* Step 6: DecomposeDG WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
- Weak TRS:
add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
add#2(Zero(),x8) -> x8
eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
eval#1(Nat(x1)) -> x1
eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
sub#2(x8,Zero()) -> x8
sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
sub#2(Zero(),Succ(x16)) -> Zero()
- Signature:
{add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
,c_1/1,c_2/0,c_3/3,c_4/0,c_5/3,c_6/1,c_7/0,c_8/1,c_9/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {add#2#,eval#1#,main#,sub#2#} and constructors {Add,Nat
,Sub,Succ,Zero}
+ Applied Processor:
DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing}
+ Details:
We decompose the input problem according to the dependency graph into the upper component
eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
and a lower component
add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
Further, following extension rules are added to the lower component.
eval#1#(Add(x2,x1)) -> add#2#(eval#1(x2),eval#1(x1))
eval#1#(Add(x2,x1)) -> eval#1#(x1)
eval#1#(Add(x2,x1)) -> eval#1#(x2)
eval#1#(Sub(x2,x1)) -> eval#1#(x1)
eval#1#(Sub(x2,x1)) -> eval#1#(x2)
eval#1#(Sub(x2,x1)) -> sub#2#(eval#1(x2),eval#1(x1))
** Step 6.a:1: SimplifyRHS WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
- Weak TRS:
add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
add#2(Zero(),x8) -> x8
eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
eval#1(Nat(x1)) -> x1
eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
sub#2(x8,Zero()) -> x8
sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
sub#2(Zero(),Succ(x16)) -> Zero()
- Signature:
{add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
,c_1/1,c_2/0,c_3/3,c_4/0,c_5/3,c_6/1,c_7/0,c_8/1,c_9/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {add#2#,eval#1#,main#,sub#2#} and constructors {Add,Nat
,Sub,Succ,Zero}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
-->_3 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
-->_2 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
-->_3 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):1
-->_2 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):1
2:S:eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
-->_3 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
-->_2 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
-->_3 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):1
-->_2 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):1
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
eval#1#(Add(x2,x1)) -> c_3(eval#1#(x2),eval#1#(x1))
eval#1#(Sub(x2,x1)) -> c_5(eval#1#(x2),eval#1#(x1))
** Step 6.a:2: UsableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
eval#1#(Add(x2,x1)) -> c_3(eval#1#(x2),eval#1#(x1))
eval#1#(Sub(x2,x1)) -> c_5(eval#1#(x2),eval#1#(x1))
- Weak TRS:
add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
add#2(Zero(),x8) -> x8
eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
eval#1(Nat(x1)) -> x1
eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
sub#2(x8,Zero()) -> x8
sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
sub#2(Zero(),Succ(x16)) -> Zero()
- Signature:
{add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
,c_1/1,c_2/0,c_3/2,c_4/0,c_5/2,c_6/1,c_7/0,c_8/1,c_9/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {add#2#,eval#1#,main#,sub#2#} and constructors {Add,Nat
,Sub,Succ,Zero}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
eval#1#(Add(x2,x1)) -> c_3(eval#1#(x2),eval#1#(x1))
eval#1#(Sub(x2,x1)) -> c_5(eval#1#(x2),eval#1#(x1))
** Step 6.a:3: Ara WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
eval#1#(Add(x2,x1)) -> c_3(eval#1#(x2),eval#1#(x1))
eval#1#(Sub(x2,x1)) -> c_5(eval#1#(x2),eval#1#(x1))
- Signature:
{add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
,c_1/1,c_2/0,c_3/2,c_4/0,c_5/2,c_6/1,c_7/0,c_8/1,c_9/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {add#2#,eval#1#,main#,sub#2#} and constructors {Add,Nat
,Sub,Succ,Zero}
+ Applied Processor:
Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
+ Details:
Signatures used:
----------------
Add :: ["A"(14) x "A"(14)] -(14)-> "A"(14)
Sub :: ["A"(14) x "A"(14)] -(14)-> "A"(14)
eval#1# :: ["A"(14)] -(5)-> "A"(1)
c_3 :: ["A"(0) x "A"(0)] -(0)-> "A"(12)
c_5 :: ["A"(0) x "A"(0)] -(0)-> "A"(12)
Cost-free Signatures used:
--------------------------
Base Constructor Signatures used:
---------------------------------
"Add_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1)
"Sub_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1)
"c_3_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1)
"c_5_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
eval#1#(Sub(x2,x1)) -> c_5(eval#1#(x2),eval#1#(x1))
2. Weak:
eval#1#(Add(x2,x1)) -> c_3(eval#1#(x2),eval#1#(x1))
** Step 6.a:4: Ara WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
eval#1#(Add(x2,x1)) -> c_3(eval#1#(x2),eval#1#(x1))
- Weak DPs:
eval#1#(Sub(x2,x1)) -> c_5(eval#1#(x2),eval#1#(x1))
- Signature:
{add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
,c_1/1,c_2/0,c_3/2,c_4/0,c_5/2,c_6/1,c_7/0,c_8/1,c_9/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {add#2#,eval#1#,main#,sub#2#} and constructors {Add,Nat
,Sub,Succ,Zero}
+ Applied Processor:
Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
+ Details:
Signatures used:
----------------
Add :: ["A"(11) x "A"(11)] -(11)-> "A"(11)
Sub :: ["A"(11) x "A"(11)] -(11)-> "A"(11)
eval#1# :: ["A"(11)] -(5)-> "A"(0)
c_3 :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
c_5 :: ["A"(0) x "A"(0)] -(0)-> "A"(14)
Cost-free Signatures used:
--------------------------
Base Constructor Signatures used:
---------------------------------
"Add_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1)
"Sub_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1)
"c_3_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1)
"c_5_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
eval#1#(Add(x2,x1)) -> c_3(eval#1#(x2),eval#1#(x1))
2. Weak:
** Step 6.b:1: Ara WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
- Weak DPs:
eval#1#(Add(x2,x1)) -> add#2#(eval#1(x2),eval#1(x1))
eval#1#(Add(x2,x1)) -> eval#1#(x1)
eval#1#(Add(x2,x1)) -> eval#1#(x2)
eval#1#(Sub(x2,x1)) -> eval#1#(x1)
eval#1#(Sub(x2,x1)) -> eval#1#(x2)
eval#1#(Sub(x2,x1)) -> sub#2#(eval#1(x2),eval#1(x1))
- Weak TRS:
add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
add#2(Zero(),x8) -> x8
eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
eval#1(Nat(x1)) -> x1
eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
sub#2(x8,Zero()) -> x8
sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
sub#2(Zero(),Succ(x16)) -> Zero()
- Signature:
{add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
,c_1/1,c_2/0,c_3/3,c_4/0,c_5/3,c_6/1,c_7/0,c_8/1,c_9/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {add#2#,eval#1#,main#,sub#2#} and constructors {Add,Nat
,Sub,Succ,Zero}
+ Applied Processor:
Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
+ Details:
Signatures used:
----------------
Add :: ["A"(6) x "A"(6)] -(0)-> "A"(6)
Add :: ["A"(8) x "A"(8)] -(0)-> "A"(8)
Nat :: ["A"(6)] -(6)-> "A"(6)
Sub :: ["A"(6) x "A"(6)] -(0)-> "A"(6)
Sub :: ["A"(8) x "A"(8)] -(0)-> "A"(8)
Succ :: ["A"(4)] -(4)-> "A"(4)
Succ :: ["A"(5)] -(5)-> "A"(5)
Succ :: ["A"(1)] -(1)-> "A"(1)
Zero :: [] -(0)-> "A"(5)
Zero :: [] -(0)-> "A"(1)
Zero :: [] -(0)-> "A"(15)
add#2 :: ["A"(5) x "A"(5)] -(0)-> "A"(5)
eval#1 :: ["A"(6)] -(0)-> "A"(5)
sub#2 :: ["A"(5) x "A"(1)] -(0)-> "A"(5)
add#2# :: ["A"(4) x "A"(0)] -(6)-> "A"(0)
eval#1# :: ["A"(8)] -(14)-> "A"(0)
sub#2# :: ["A"(4) x "A"(5)] -(7)-> "A"(0)
c_1 :: ["A"(0)] -(0)-> "A"(0)
c_8 :: ["A"(0)] -(0)-> "A"(14)
Cost-free Signatures used:
--------------------------
Base Constructor Signatures used:
---------------------------------
"Add_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1)
"Nat_A" :: ["A"(1)] -(1)-> "A"(1)
"Sub_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1)
"Succ_A" :: ["A"(1)] -(1)-> "A"(1)
"Zero_A" :: [] -(0)-> "A"(1)
"c_1_A" :: ["A"(0)] -(0)-> "A"(1)
"c_8_A" :: ["A"(0)] -(0)-> "A"(1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
2. Weak:
sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
** Step 6.b:2: Ara WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
- Weak DPs:
add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
eval#1#(Add(x2,x1)) -> add#2#(eval#1(x2),eval#1(x1))
eval#1#(Add(x2,x1)) -> eval#1#(x1)
eval#1#(Add(x2,x1)) -> eval#1#(x2)
eval#1#(Sub(x2,x1)) -> eval#1#(x1)
eval#1#(Sub(x2,x1)) -> eval#1#(x2)
eval#1#(Sub(x2,x1)) -> sub#2#(eval#1(x2),eval#1(x1))
- Weak TRS:
add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
add#2(Zero(),x8) -> x8
eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
eval#1(Nat(x1)) -> x1
eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
sub#2(x8,Zero()) -> x8
sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
sub#2(Zero(),Succ(x16)) -> Zero()
- Signature:
{add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
,c_1/1,c_2/0,c_3/3,c_4/0,c_5/3,c_6/1,c_7/0,c_8/1,c_9/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {add#2#,eval#1#,main#,sub#2#} and constructors {Add,Nat
,Sub,Succ,Zero}
+ Applied Processor:
Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
+ Details:
Signatures used:
----------------
Add :: ["A"(4) x "A"(4)] -(4)-> "A"(4)
Nat :: ["A"(4)] -(0)-> "A"(4)
Sub :: ["A"(4) x "A"(4)] -(0)-> "A"(4)
Succ :: ["A"(1)] -(1)-> "A"(1)
Succ :: ["A"(0)] -(0)-> "A"(0)
Zero :: [] -(0)-> "A"(1)
Zero :: [] -(0)-> "A"(0)
Zero :: [] -(0)-> "A"(14)
add#2 :: ["A"(1) x "A"(1)] -(3)-> "A"(1)
eval#1 :: ["A"(4)] -(0)-> "A"(1)
sub#2 :: ["A"(1) x "A"(0)] -(0)-> "A"(1)
add#2# :: ["A"(1) x "A"(0)] -(7)-> "A"(0)
eval#1# :: ["A"(4)] -(11)-> "A"(0)
sub#2# :: ["A"(1) x "A"(0)] -(1)-> "A"(0)
c_1 :: ["A"(0)] -(0)-> "A"(14)
c_8 :: ["A"(0)] -(0)-> "A"(14)
Cost-free Signatures used:
--------------------------
Base Constructor Signatures used:
---------------------------------
"Add_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1)
"Nat_A" :: ["A"(1)] -(0)-> "A"(1)
"Sub_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1)
"Succ_A" :: ["A"(1)] -(1)-> "A"(1)
"Zero_A" :: [] -(0)-> "A"(1)
"c_1_A" :: ["A"(0)] -(0)-> "A"(1)
"c_8_A" :: ["A"(0)] -(0)-> "A"(1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
2. Weak:
WORST_CASE(?,O(n^2))